T:Type, dT:EqDecider(T), L:(T List). ((null(L)))  (index(L;hd(L)) ~ 0) 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), b, b, , s = t, , eqof(d), f(a), x:AB(x), x:A  B(x), P & Q, P  Q, Unit, left + right, hd(l), i <z j, i z j, l[i], index(L;x), [car / cdr], ||as||, #$n, {i..j}, s ~ t, {T}, A  B, i  j < k, , a < b, {x:A| B(x)} , True, T, SQType(T), [], type List, Type, EqDecider(T), Void, x:A.B(x), Top, S  T, null(as), P  Q
Lemmas	deq property, null wf3, top wf, deq wf, length wf2, int seg wf, length wf1, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, eqof wf, bool wf, bnot wf, not wf, assert wf